googologywikiaorg-20200223-history
Loader's number
Loader's number is the output of loader.c, a program by Ralph Loader that came in first place for the Bignum Bakeoff contest, whose objective was to write a C program (in 512 characters or less) that generates the largest possible output on a theoretical machine with infinite memory. It is among the largest computable numbers ever devised. The program diagonalizes over the Huet-Coquand calculus of constructions, a particularly expressive lambda calculus. Its output, affectionately nicknamed Loader's number, is defined as \(D^5(99)=D(D(D(D(D(99)))))\), where \(D(k)\) is an accumulation of all possible expressions provable within approximately \(log(k)\) inference steps in the calculus of constructions (encoding proofs as binary numbers and expressions as power towers). The proof strength and expressiveness of the calculus of constructions makes the output of \(D(k)\) grow very large for sufficiently large k''. David Moews has shown that \(D(99)\) is larger than \(2↑↑30,419\) (where ↑↑ is tetration), and that even \(D^2(99)\) would be much larger than \(f_{\varepsilon_0+\omega^3}(1,000,000)\) in the fast-growing hierarchy, using Cantor's definition of fundamental sequences. \(D^2(99)\) thus is obviously much larger than the output of Marxen.c, which is upper bounded at the aforementioned \(f_{\varepsilon_0+\omega^3}(1,000,000)\). The final output of \(D^5(99)\) is much larger than TREE(3), SCG(13), and, say, BH(100). It is overpowered by finite promise games and greedy clique sequences. Loader's function is computable, so \(\Sigma(n) > D^5(99)\) for relatively small ''n, say, n = 2000. Code #define R { return #define P P ( #define L L ( #define T S (v, y, c, #define C ), #define X x) #define F );} int r, a; P y, X R y - ~y << x; } Z (X R r = x % 2 ? 0 : 1 + Z (x / 2 F L X R x / 2 >> Z (x F #define U = S(4,13,-4, T t) { int f = L t C x = r; R f - 2 ? f > 2 ? f - v ? t - (f > v) * c : y : P f, P T L X C S (v+2, t U y C c, Z (X ))) : A (T L X C T Z (X ) F } A (y, X R L y) - 1 ? 5 << P y, X : S (4, x, 4, Z ® F #define B (x /= 2) % 2 && ( D (X { int f, d, c = 0, t = 7, u = 14; while (x && D (x - 1 C B 1)) d = L L D (X ) C f = L r C x = L r C c - r || ( L u) || L r) - f || B u = S (4, d, 4, r C t = A (t, d) C f / 2 & B c = P d, c C t U t C u U u) ) C c && B t = P ~u & 2 | B u = 1 << P L c C u) C P L c C t) C c = r C u / 2 & B c = P t, c C u U t C t = 9 ); R a = P P t, P u, P x, c)) C a F } main () R D (D (D (D (D (99)))) F See also External links * David Moews' comments on the program, as well as other entries * The original program prior to compression * Loader's home page ja:ローダー数 Category:Bignum Bakeoff contestant Category:Functions Category:Numbers Category:Computers Category:Eponymous numbers Category:Higher computable level Category:Eponymous functions